\begin{tabbing} q{-}sat{-}constraints($k$;$A$;$y$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\parallel$$y$$\parallel$ = $k$ $\in$ $\mathbb{Z}$)\+ \\[0ex]c$\wedge$ \=l\_all($A$;:($\mathbb{Q}$ List)\+ \\[0ex]$\times$ (:$\mathbb{Z}$ \\[0ex]$\times$ ($\mathbb{Q}$ List));$a$.\=let $F$,$r$,$G$ = $a$ in \+ \\[0ex]if\= ($r$ =$_{0}$ 0)\+ \\[0ex]then q{-}linear($k$;$j$.$F$[$j$]?0;$y$) = q{-}linear($k$;$j$.$G$[$j$]?0;$y$) $\in$ $\mathbb{Q}$ \-\\[0ex]if\= ($r$ =$_{0}$ 1)\+ \\[0ex]then q{-}linear($k$;$j$.$F$[$j$]?0;$y$) $\leq$ q{-}linear($k$;$j$.$G$[$j$]?0;$y$) \-\\[0ex]else q{-}linear($k$;$j$.$F$[$j$]?0;$y$) $<$ q{-}linear($k$;$j$.$G$[$j$]?0;$y$) \\[0ex]fi ) \-\-\- \end{tabbing}